/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.ast;

import java.util.Collections;
import java.util.Map;
import java.util.Set;

/**
 * Represents an Alloy command that runs an analysis for particular scopes,
 * such as "run ShowExampleExecution for 3 Train, 2 Track" or "check SafetyInvariantPreserved for 4".
 * <p>
 * The important field here is {@link #formula}, which is the <b>translatable AST</b>
 * representing the desugared Alloy {@link Formula} for this command.  This formula is typically
 * a conjunction of all facts in the model together with a constraint (e.g. a named Alloy predicate)
 * specific to this command.  For example if the model looks like
 * <p>
 * <pre>
 * fact F1{...} fact F2{...} pred P1 {...} pred P2 { ... }
 * run P1 for 3
 * check P2 for 4
 * </pre>
 * then there will be two {@link FindCommand}s, one for the "run" command and one for the "check" command;
 * and the {@link #formula} in the "run" command will be "(F1 && F2) && P1" while the formula in the "check"
 * command will be "(F1 && F2) && !P2".
 */
public abstract class FindCommand extends Command {

    public static final int EXPECTS_INDEX = 1;

    /**
     * Formula for this command, constructed by {@link alloy.transform.GenCommandFormulasVisitor}.
     */
    public Formula formula = null;

    /**
     * The leaf ids of skolem constants in {@link #formula}.
     */
    public Set /* of LeafId */ skolemIds = Collections.EMPTY_SET;

    /** The types of skolem constants. */
    public Map /* String -> UnionType */ skolemTypes = Collections.EMPTY_MAP;

    /**
     * Map from leaf ids of relations and quantified variables to their
     * {@link alloy.subscope.ExprRelationInfo annotations} related to subscopes
     */
    public Map id2Annotation = null;
    
    public FindCommand(final String name_, Location location_, Scope scope_, IntNode expects_) {
        super(name_, location_, scope_);
        addChild(expects_);
    }


    public FindCommand(final String name_, Scope scope_, IntNode expects_) {
        this(name_, Location.UNKNOWN, scope_, expects_);
    }



    //GET AND SET METHODS

    /**
     * gets the expects of this
     * @return the number of solutions expected
     */
    protected IntNode getExpects() {
        return (IntNode)childAt(EXPECTS_INDEX);
    }

    /** set the Expects of this */
    public void setExpects(IntNode newChild_) {
        setChild(EXPECTS_INDEX, newChild_);
        this.info().setExpects(getExpects().isEmpty(), getExpects().getInt());
    }

    /**
     * accept an AST visitor
     * @param visitor_ the visitor
     */
    protected void acceptVisitor(ASTVisitor visitor_) {
        visitor_.visit(this);
    }

    /**
     * accept a returning AST visitor
     * @param visitor_ the visitor
     * @return the Object returned by the visitor
     */
    protected Object acceptReturnVisitor(ASTReturnVisitor visitor_) {
        return visitor_.visit(this);
    }

    public String toString()
    {
        return nodeString();
    }

}















